open import Algebra.Structures using (  IsGroup ; IsAbelianGroup ; IsSemigroup)
open import Algebra using ( Group ; Monoid ; Semigroup ; AbelianGroup)
open import Substructures using (IsSubGroup ; SubGroup ; IsNormalSubGroup ; NormalSubGroup)
open import Util
open import QuotientRelation using (QuotientRelation ; quotientGroupIsAGroup)
open import Kern using (Kernₕ)
open import Relation.Unary using ( Pred ; U; Decidable ; _∩_ ; _⊆_)
open import Data.Product using (∃ ; Σ ; _×_ ; _,_ ; _,′_ ; proj₁ ; proj₂)
open import Agda.Builtin.Unit
open import Level using ( Level ; _⊔_ ; suc  )
open import Relation.Binary using ( Rel )
open import Algebra.FunctionProperties using ( Op₁ ; Op₂ )
open import Algebra.Properties.Group using  (⁻¹-involutive)

{--
0. G  - grupa
1. N  - normala podrupa G
2. (normalna) podgrupa G/N to (normala) grupa H ⊂ G która jest podzbiorem G\N czyli: a ∈ H  → b ∈ G → a ≈ₖₙ b [ab\1 ∈ N] →  b ∈ H

It is easily seen that a subgroup H of G is subset of G/N just in case N ⊆ H.
H ⊆ G
x∈N → x∈H

a ∈ H → b ∈ G → ab\1 ∈ N ;; z tego wynika że ab\1 ∈ H 


--}


module II-1-2 {a ℓ b₁ b₂} (g : Group a ℓ) (predₕ : Pred (Group.Carrier g) b₁) (predₖ : Pred (Group.Carrier g) b₂)
  (h-subGroup : let open Group g in IsSubGroup _≈_ predₕ _∙_ ε _⁻¹)
  (k-normalSubGroup : let open Group g in IsNormalSubGroup _≈_ predₖ _∙_ ε _⁻¹)
  where

open Group g

{-- the set HK {hk: h € H and k E K} is a subgroup,
k : A , predk h: A , predh -> x ≈ kh
--}
private
  predₕₖ = λ x → ∃ (λ hₓ →  (∃ (λ kₓ → ((predₕ hₓ) × (predₖ kₓ)) × (x ≈ (hₓ ∙ kₓ)) )))

theorem-II-1-2-I : IsSubGroup _≈_ predₕₖ _∙_ ε _⁻¹
theorem-II-1-2-I = let
  εInSubset : predₕₖ ε
  εInSubset =  ε , (ε , (IsSubGroup.εInSubset h-subGroup , IsNormalSubGroup.εInSubset k-normalSubGroup) , (sym (identityˡ ε)))
  ≈_respect : {x y : Carrier} (_ : x ≈ y) →  (predₕₖ x) → (predₕₖ y)
  ≈_respect {x} {y} x≈y pₓ = let
    hₓ = proj₁ pₓ
    tmp1 = proj₂ pₓ
    kₓ = proj₁ tmp1
    dd = proj₂ tmp1
    qq : x ≈ (hₓ ∙ kₓ)
    qq = proj₂ dd
    in hₓ , (kₓ , ((proj₁ dd) , (trans (sym x≈y) qq)))
  closedUnder⁻¹ : {x : Carrier} (pₓ : predₕₖ x) → (predₕₖ (x ⁻¹))
  closedUnder⁻¹ {x} pₓ = let
    hₓ = proj₁ pₓ
    pₓ₂ = proj₂ pₓ
    kₓ = proj₁ pₓ₂
    pₓ₂₂ = proj₂ pₓ₂
    preds = proj₁ pₓ₂₂
    eq : x ≈ (hₓ ∙ kₓ)
    eq = proj₂ pₓ₂₂
    x⁻¹≈kₓ⁻¹∙hₓ⁻¹ : (x ⁻¹) ≈ ((kₓ ⁻¹) ∙ (hₓ ⁻¹))
    x⁻¹≈kₓ⁻¹∙hₓ⁻¹ = trans (⁻¹-cong eq) (∙⁻¹-distribution g hₓ kₓ)
    eqb : ( ((hₓ ⁻¹) ∙ hₓ) ∙ (kₓ ⁻¹ ∙ hₓ ⁻¹)) ≈ (hₓ ⁻¹ ∙ (hₓ ∙ (kₓ ⁻¹ ∙ hₓ ⁻¹)))
    eqb = assoc (hₓ ⁻¹) (hₓ) (kₓ ⁻¹ ∙ hₓ ⁻¹) 
    eqc : (hₓ ⁻¹ ∙ (hₓ ∙ (kₓ ⁻¹ ∙ hₓ ⁻¹)) ) ≈ (hₓ ⁻¹ ∙ (hₓ ∙ kₓ ⁻¹ ∙ hₓ ⁻¹))
    eqc = ∙-cong (refl {hₓ ⁻¹}) (sym (assoc (hₓ) (kₓ ⁻¹) (hₓ ⁻¹)))
    in (hₓ ⁻¹) , (hₓ ∙ (kₓ ⁻¹) ∙ (hₓ ⁻¹) ,
    (IsSubGroup.⁻¹_isSubStructure h-subGroup (proj₁ preds) ,
   IsNormalSubGroup.isNormal k-normalSubGroup hₓ (kₓ ⁻¹) (IsNormalSubGroup.⁻¹_isSubStructure k-normalSubGroup (proj₂ preds))) , 
    trans x⁻¹≈kₓ⁻¹∙hₓ⁻¹ (trans (trans (sym (identityˡ  (kₓ ⁻¹ ∙ hₓ ⁻¹))) (∙-cong  (sym(inverseˡ hₓ)) (refl {kₓ ⁻¹ ∙ hₓ ⁻¹}))) (trans eqb eqc)))
  --
  closedUnder∙ : predₕₖ Substructures.ClosedUnder _∙_
  closedUnder∙ = λ {x} {y} pₓ py → let
    hₓ = proj₁ pₓ
    pₓ₂ = proj₂ pₓ
    kₓ = proj₁ pₓ₂
    pₓ₂₂ = proj₂ pₓ₂
    predsₓ = proj₁ pₓ₂₂
    eqₓ : x ≈ (hₓ ∙ kₓ)
    eqₓ = proj₂ pₓ₂₂
    hy = proj₁ py
    py₂ = proj₂ py
    ky = proj₁ py₂
    py₂₂ = proj₂ py₂
    predsy = proj₁ py₂₂
    eqy : y ≈ (hy ∙ ky)
    eqy = proj₂ py₂₂
   {--
hx kx hy ky

hx hy hy- kx hy ky
--}
    fi4 : (hy ∙ ((hy ⁻¹) ∙ (kₓ ∙ (((hy ⁻¹) ⁻¹) ∙ ky)))) ≈ (kₓ ∙ (((hy ⁻¹) ⁻¹) ∙ ky))
    fi4 =  trans (sym (assoc hy (hy ⁻¹) (kₓ ∙ (((hy ⁻¹) ⁻¹) ∙ ky)))) (trans (∙-cong (inverseʳ hy) refl) (identityˡ _))
    ee : (kₓ ∙ (hy ∙ ky)) ≈ (kₓ ∙ (hy ⁻¹ ⁻¹ ∙ ky))
    ee = (∙-cong (refl {kₓ}) (∙-cong (sym (⁻¹-involutive g hy))  (refl {ky}) ))
    fq2 : (kₓ ∙ ((hy ⁻¹) ⁻¹) ∙ ky) ≈ (kₓ ∙ (hy ∙ ky))
    fq2 = trans (assoc kₓ ((hy ⁻¹) ⁻¹) ky) (sym ee)
    fi3 :  (hy ∙ ((hy ⁻¹ ∙ kₓ) ∙ (((hy ⁻¹) ⁻¹) ∙ ky))) ≈ (hy ∙ ((hy ⁻¹) ∙ (kₓ ∙ (((hy ⁻¹) ⁻¹) ∙ ky))))
    fi3 = ∙-cong refl (assoc (hy ⁻¹) kₓ ((((hy ⁻¹) ⁻¹) ∙ ky)))
    fi2 : (hy ∙ (((hy ⁻¹ ∙ kₓ) ∙ (hy ⁻¹) ⁻¹) ∙ ky)) ≈ (hy ∙ ((hy ⁻¹ ∙ kₓ) ∙ (((hy ⁻¹) ⁻¹) ∙ ky)))
    fi2 =  ∙-cong (refl {hy}) ( assoc (hy ⁻¹ ∙ kₓ) ((hy ⁻¹) ⁻¹) ky )

    fqq : (hy ∙ (((hy ⁻¹ ∙ kₓ) ∙ (hy ⁻¹) ⁻¹) ∙ ky)) ≈ (kₓ ∙ ((hy ⁻¹) ⁻¹) ∙ ky)
    fqq = trans fi2 (trans fi3 (trans fi4 ((sym (assoc (proj₁ (proj₂ pₓ)) ((proj₁ py ⁻¹) ⁻¹) (proj₁ (proj₂ py)))))))
    fi1 : (kₓ ∙ (hy ∙ ky)) ≈ (hy ∙ (((hy ⁻¹ ∙ kₓ) ∙ (hy ⁻¹) ⁻¹) ∙ ky))
    fi1 = trans (sym fq2) (sym fqq)
    fin : (hₓ ∙ kₓ ∙ (hy ∙ ky)) ≈ (hₓ ∙ hy ∙ (hy ⁻¹ ∙ kₓ ∙ (hy ⁻¹) ⁻¹ ∙ ky))
    fin = trans (assoc hₓ kₓ (hy ∙ ky)) (trans (∙-cong (refl {hₓ}) fi1)  (sym (assoc hₓ  hy  (hy ⁻¹ ∙ kₓ ∙ (hy ⁻¹) ⁻¹ ∙ ky))))
    in (hₓ ∙ hy) , (((hy ⁻¹) ∙ kₓ ∙ ((hy ⁻¹) ⁻¹ )) ∙ ky) ,
      ((IsSubGroup.∙_isSubStructure h-subGroup (proj₁ predsₓ) (proj₁ predsy) ,
      IsNormalSubGroup.∙_isSubStructure k-normalSubGroup (IsNormalSubGroup.isNormal k-normalSubGroup (hy ⁻¹)  kₓ (proj₂ predsₓ) ) (proj₂ predsy)) ,
      trans (∙-cong eqₓ eqy) fin)
  in
  record
                     { isGroup = isGroup
                     ; ⁻¹_isSubStructure = closedUnder⁻¹
                     ; isSubMonoid = record { isMonoid = (IsGroup.isMonoid isGroup)
                       ;  ∙_isSubStructure = closedUnder∙ 
                       ; ≈_respect = ≈_respect
                       ; εInSubset = εInSubset
                       }
                     }

H∩K-subgroup : IsSubGroup _≈_ (predₕ ∩ predₖ) _∙_ ε _⁻¹
H∩K-subgroup = record
  { isGroup = isGroup
  ; ⁻¹_isSubStructure = λ {x} px → (IsSubGroup.⁻¹_isSubStructure h-subGroup (proj₁ px)) , (IsNormalSubGroup.⁻¹_isSubStructure k-normalSubGroup (proj₂ px))
  ; isSubMonoid = record { isMonoid = (IsGroup.isMonoid isGroup)
    ; ∙_isSubStructure = λ px py → (IsSubGroup.∙_isSubStructure h-subGroup (proj₁ px) (proj₁ py)) , (IsNormalSubGroup.∙_isSubStructure k-normalSubGroup (proj₂ px) (proj₂ py))
    ; ≈_respect = λ x≈y px → (IsSubGroup.≈_respect h-subGroup x≈y (proj₁ px)) , (IsNormalSubGroup.≈_respect k-normalSubGroup x≈y (proj₂ px))
    ; εInSubset = (IsSubGroup.εInSubset h-subGroup) , (IsNormalSubGroup.εInSubset k-normalSubGroup)
    }
  }

--todo czy dobrze zgadłem co oznacza 'is normal in H'?
-- druga interpreteacja chyba jest co najmniej nieudowadnialna
theorem-II-1-2-II : Substructures.IsNormalInG H∩K-subgroup predₕ
theorem-II-1-2-II x {xₕ} y yₕₖ =  IsSubGroup.∙_isSubStructure h-subGroup (IsSubGroup.∙_isSubStructure h-subGroup xₕ (proj₁ yₕₖ)) (IsSubGroup.⁻¹_isSubStructure h-subGroup xₕ) , IsNormalSubGroup.isNormal k-normalSubGroup x y (proj₂ yₕₖ)

pred∩ = predₕ ∩ predₖ 
--3. The quotient groups HK/K and H/(H∩K) are isomorphic
≈k = (QuotientRelation Carrier predₖ _∙_ _⁻¹)
≈∩ = (QuotientRelation Carrier pred∩ _∙_ _⁻¹) 
isGroupG\K = quotientGroupIsAGroup g predₖ k-normalSubGroup
--to jest błędne bo K∩H nie jest normalne!!!:
--isGroupG\∩ = quotientGroupIsAGroup g pred∩ {!!}
{--
Teraz trzeba znaleźć kontrprzykład
x ∈ G q∈ K∩H
x q x⁻¹ ∉ K∩H (∈ K ale ∉ H)

trzeba wymyślić coś żeby nie było przemienne bo inaczej xqx⁻¹ ≈ q

--}
